Nuprl Definition : p-open-measure-one
11,40
postcript
pdf
measure(
C
) = 1 ==
m
:
.
n
:
. 1 - (1/
m
)
E(
n
;
s
.
C
(<
n
,
s
>))
latex
clarification:
p-open-measure-one(
p
;
C
) ==
m
:
.
n
:
. 1 - (1/
m
)
expectation(
p
;
n
;
s
.
C
(<
n
,
s
>))
latex
Definitions
x
:
A
.
B
(
x
)
,
,
x
:
A
.
B
(
x
)
,
,
r
s
,
r
-
s
,
(
r
/
s
)
,
#$n
,
E(
n
;
F
)
,
x
.
A
(
x
)
,
f
(
a
)
,
<
a
,
b
>
FDL editor aliases
p-open-measure-one
origin